package org.cos.verification.automata;

import java.util.Enumeration;
import java.util.Hashtable;
import java.util.Vector;

import org.cos.verification.verifier.Rule;
import org.shellex.javame.utility.Pair;

import com.sun.midp.midlet.Selector;
import com.sun.perseus.model.ImageNode;



class TransformTable {
	//transitions[src_id] = {dst_id: [method ...] , ...}
	public Hashtable index =  null;
	
	
	public TransformTable(){
		this.index = new Hashtable();
	}
	
	public void add_transition(int src_id, int dst_id, Transition tran) {
		if ( ! index.containsKey(new Integer(src_id))) {
			index.put(new Integer(src_id), new Hashtable());
		} 
//		if ( ! index.containsKey(new Integer(dst_id))) {
//			index.put(new Integer(dst_id), new Hashtable());
//		}
		
		Hashtable transforms = (Hashtable) index.get(new Integer(src_id));
		Vector trans;
		if ( ! transforms.containsKey(new Integer(dst_id))) {
			trans = new Vector();
		} else {
			trans = (Vector) transforms.get(new Integer(dst_id));
		}
		trans.addElement(tran);
		transforms.put(new Integer(dst_id), trans);
		//DEBUG System.out.println("Add trans: "+ src_id+"->"+ dst_id+":" + tran.method);
		index.put(new Integer(src_id), transforms);
		
	}
	
    public Vector get_transitions(int src_id) {
    	Vector ret = new Vector();
		Hashtable transform = (Hashtable) index.get(new Integer(src_id));
		//DEBUG System.out.println(src_id + ": "+transform);
		
    	for (Enumeration e2 = transform.keys(); e2.hasMoreElements();){
    		Integer dst_id = (Integer) e2.nextElement();
    		Vector trans = (Vector) transform.get(dst_id);
    		for (Enumeration e3 = trans.elements(); e3.hasMoreElements();){
    			ret.addElement(new Pair(dst_id, e3.nextElement()));
    		}
    	}
    	return ret;
    }
       
}



public class Automata {

	public String name;
	// trans_table: {tran.dst_state_id: method ... }
	public TransformTable tranform_table;
	private Vector trans;
	public Hashtable state_set;
	public Vector final_state_set ;
	private Vector init_state ;
	
	public Automata(){
		this("");
	}
	
	public Automata(String name) {
		this.name = name;
		tranform_table = new TransformTable(); 
		trans = new Vector();
		state_set = new Hashtable();
		final_state_set = new Vector();
		init_state = new Vector();
	}

	public boolean is_final(Integer id) {
		return final_state_set.contains(id);
	}
	public boolean is_init(Integer id) {
		return init_state.contains(id);
	}
	
	public Automata add_state(int src_id) {
		Integer id = new Integer(src_id);
		state_set.put(id, id);
		if ( ! tranform_table.index.containsKey(id)) {
			tranform_table.index.put(id, new Hashtable());
		} 
		return this;
	}

	
	public Automata set_final(int state_id) {
		if (! final_state_set.contains(new Integer(state_id)))
			final_state_set.addElement(new Integer(state_id));
		return this;
	}

	public Automata set_transition(int src_id, int dst_id,
			Transition tran) {
		tranform_table.add_transition(src_id, dst_id, tran);
		return this;

	}

	public Automata set_init(int state_id) {
		init_state.addElement(new Integer(state_id));
		return this;
	}
	
	public void print(){
		System.out.println("name: " + this.name);
		System.out.print("states: [");
		for (Enumeration enumobj = this.state_set.elements(); enumobj.hasMoreElements();) {
			Integer s = (Integer)enumobj.nextElement();
			System.out.print( s.intValue() + ",");
		}
		System.out.println("]");

		System.out.print("init states: ");
		for (Enumeration enumobj = init_state.elements(); enumobj.hasMoreElements();) {
			Integer fs = (Integer)enumobj.nextElement();
			System.out.print("[" + fs.intValue() + "]");
		}
		System.out.println();

		System.out.print("final states: ");
		for (Enumeration enumobj = final_state_set.elements(); enumobj.hasMoreElements();) {
			Integer fs = (Integer)enumobj.nextElement();
			System.out.print("[" + fs.intValue() + "]");
		}
		System.out.println();
		
		System.out.println("trans: ");
		for (Enumeration enumobj = this.state_set.elements(); enumobj.hasMoreElements();) {
			int src_id = ((Integer)enumobj.nextElement()).intValue();
			//DEBUG System.out.println(src_id);
			Vector trans_pair = this.tranform_table.get_transitions(src_id);

			for (Enumeration enum_tran = trans_pair.elements(); enum_tran.hasMoreElements();) {
				Pair p = (Pair)enum_tran.nextElement();

				Integer dst_id = (Integer) p.head;
				Transition tran = (Transition) p.tail;

				//System.out.println(methods.get(new Integer(tran.method_id)).toString());
				System.out.print("[" 
						+ src_id + "->" + dst_id + ":"+ tran.method + "]"); 
				
				for (Enumeration enum_cond = tran.conditions.elements(); enum_cond.hasMoreElements();) {
					Condition cond = (Condition)enum_cond.nextElement();
					System.out.print("{" + cond.target_id +":"+cond.type);
					for (Enumeration enum_set = cond.sets.elements(); enum_set.hasMoreElements();) {
						CondSet set = (CondSet) enum_set.nextElement();
						System.out.print("|" + set.relation + "<" +set.value_d + "," +set.value_u + ">");
					}
					System.out.print("}");
				}
				
				for (Enumeration enum_act = tran.actions.elements(); enum_act.hasMoreElements();) {
					Action act = (Action)enum_act.nextElement();
					System.out.print("[" + act.type + ":" + act.opt + ":" + act.value + "]");
				}
				System.out.println( );
			}
			
		}
		System.out.println();
		
	}
	
	private void merge_states(AutomataBuilder ab, Automata am, Hashtable temp_map){
		Integer temp_map_counter = new Integer(0);

		for (Enumeration enum_my_id = state_set.elements(); enum_my_id.hasMoreElements();){
			Integer my_id = (Integer)enum_my_id.nextElement();
			for (Enumeration enum_your_id = am.state_set.elements(); enum_your_id.hasMoreElements();){
				Integer your_id = (Integer)enum_your_id.nextElement();

				Integer new_child_id = temp_map_counter;
				boolean is_init = am.is_init(your_id);
				boolean is_final = am.is_final(your_id)? true: (this.is_final(my_id) ? true:false);
				
				ab.set_state(new_child_id.intValue(), is_init, is_final);
				temp_map.put( new Pair(my_id, your_id), new_child_id);

				temp_map_counter = new Integer(temp_map_counter.intValue() +1);
			}
		}
	}
	
	private void merge_transitions(AutomataBuilder ab, Automata am, Hashtable temp_map){
		for (Enumeration enum_print_k1 = this.state_set.elements(); enum_print_k1.hasMoreElements();) {
			Integer my_state_id = (Integer) enum_print_k1.nextElement();
			Vector my_transforms = this.tranform_table.get_transitions(my_state_id.intValue());
			
			for (Enumeration enum_print_k2 = am.state_set.elements(); enum_print_k2.hasMoreElements();) {
				Integer your_state_id = (Integer) enum_print_k2.nextElement();
				Vector your_transforms = am.tranform_table.get_transitions(your_state_id.intValue());
				 
				for (Enumeration enum_my_transforms = my_transforms.elements(); enum_my_transforms.hasMoreElements();){
					Pair my_tran_p = (Pair) enum_my_transforms.nextElement();
					Integer my_dst_id = (Integer) my_tran_p.head;
					Transition my_tran = (Transition) my_tran_p.tail;
					Method my_method = (Method) my_tran.method;
					Vector my_conds = (Vector) my_tran.conditions;
					Vector my_acts = (Vector) my_tran.actions;

					for (Enumeration enum_your_transforms = your_transforms.elements(); enum_your_transforms.hasMoreElements();){
						Pair your_tran_p = (Pair) enum_your_transforms.nextElement();
						Integer your_dst_id = (Integer) your_tran_p.head;
						Transition your_tran = (Transition) your_tran_p.tail;
						Method your_method = (Method) your_tran.method;
						Vector your_conds = (Vector) your_tran.conditions;
						Vector your_acts = (Vector) your_tran.actions;

						if (my_method.cmp_method(your_method)) { //Compare method
							Integer src_id = (Integer) temp_map.get(new Pair(my_state_id, your_state_id));
							Integer dst_id = (Integer) temp_map.get(new Pair(my_dst_id, your_dst_id));
							
							ab.build_transition(src_id.intValue(), dst_id.intValue(), my_method,
									 merge_conditions(my_conds, your_conds),
									 merge_actions(my_acts, your_acts));
							//DEBUG System.out.println("New Tran:" + src_id + "->"+dst_id + ":"+ my_method);

						} else {
							Integer src_id = (Integer) temp_map.get(new Pair(my_state_id, your_state_id));
							Integer dst_id = (Integer) temp_map.get(new Pair(my_dst_id, your_state_id));
							
							ab.build_transition(src_id.intValue(), dst_id.intValue(), my_method,
									 merge_conditions(my_conds, your_conds),
									 merge_actions(my_acts, your_acts));
							//DEBUG System.out.println("New Tran:" + src_id + "->"+dst_id + ":"+ my_method);

						}
					}
				}
			}
		}
	}
	
	private Vector merge_conditions(Vector my, Vector your){
		Vector ret = new Vector();
		for (Enumeration enum_my = my.elements(); enum_my.hasMoreElements();){
			Condition my_cond= (Condition) enum_my.nextElement();
			for (Enumeration enum_your = your.elements(); enum_your.hasMoreElements();){
				Condition your_cond = (Condition) enum_your.nextElement();
				if (my_cond.type.equalsIgnoreCase("PARAMETER")) {
					
				} else { //VARS
					
				}
			}
		}
		return ret;
	}
	
	private Vector merge_actions(Vector my, Vector your){
		Vector ret = new Vector();
		for (Enumeration enum_my = my.elements(); enum_my.hasMoreElements();){
			ret.addElement(enum_my.nextElement());
			for (Enumeration enum_your = your.elements(); enum_your.hasMoreElements();){
				ret.addElement(enum_your.nextElement());
			}
		}
		return ret;
	}
	
	public Automata merge(Automata am) {
		AutomataBuilder ab = new AutomataBuilder();
		Hashtable temp_map = new Hashtable();
				
		//merge states
		merge_states(ab, am, temp_map);

		//test print states
		for (Enumeration enum_print_k = temp_map.keys(); enum_print_k.hasMoreElements();){
			Pair p = (Pair) enum_print_k.nextElement();
			Integer new_id = (Integer) temp_map.get(p);
			Integer my_id = (Integer) p.head;
			Integer your_id = (Integer) p.tail;
			System.out.println("("+  my_id + ", " + your_id + "->" + new_id +" )");
		}

		//merge transitions
		merge_transitions(ab, am, temp_map);

		return ab.get_automata();
	}
	
	public boolean check(){
		Vector q = new Vector();
		for (Enumeration enum_is = init_state.elements(); enum_is.hasMoreElements();) {
			Integer state_start = (Integer) enum_is.nextElement();
			q.addElement(state_start);
			while (! q.isEmpty()) {
				Integer crr_state = (Integer) q.firstElement();
				q.removeElementAt(0);
				Vector nexts = tranform_table.get_transitions(crr_state.intValue());
				for (Enumeration enum_next = nexts.elements(); enum_next.hasMoreElements();){
					Pair next_p = (Pair) enum_next.nextElement();
					Integer next_state = (Integer) next_p.head;
					if (final_state_set.contains(next_state)) {
						return true;
					}
					q.addElement(next_state);
				}
				
			}
		}
		return false;
	}
	
}
